*****∀E walk home,desk,car,S0;

1 (walkable(home,S0)∧(at(desk,home,S0)∧(at(car,home,S0)∧at(I,desk,S0))))⊃(at(I,car,walk(car,S0))∧(∀x.(walkable(x%
,walk(car,S0))≡walkable(x,S0))∧(∀x.(drivable(x,walk(car,S0))≡drivable(x,S0))∧∀x y.(¬(x=I)⊃(at(x,y,walk(car,S0))≡%
at(x,y,S0))))))  

*****TAUT at(I,car,walk(car,S0)) at1,at2,at3,walkable,1;

2 at(I,car,walk(car,S0))  

*****TAUT ∀x.(walkable(x,walk(car,S0))≡walkable(x,S0)) at1,at2,at3,walkable,1;

3 ∀x.(walkable(x,walk(car,S0))≡walkable(x,S0))  

*****TAUT ∀x.(drivable(x,walk(car,S0))≡drivable(x,S0)) at1,at2,at3,walkable,1;

4 ∀x.(drivable(x,walk(car,S0))≡drivable(x,S0))  

*****TAUT ∀x y.(¬(x=I)⊃(at(x,y,walk(car,S0))≡at(x,y,S0))) at1,at2,at3,walkable,1;

5 ∀x y.(¬(x=I)⊃(at(x,y,walk(car,S0))≡at(x,y,S0)))  

*****∀E ↑↑ county;

6 drivable(county,walk(car,S0))≡drivable(county,S0)  

*****∀E ↑↑ car,home;

7 ¬(car=I)⊃(at(car,home,walk(car,S0))≡at(car,home,S0))  

*****∀E ↑↑↑ home,county;

8 ¬(home=I)⊃(at(home,county,walk(car,S0))≡at(home,county,S0))  

*****∀E 5 airport,county;

9 ¬(airport=I)⊃(at(airport,county,walk(car,S0))≡at(airport,county,S0))  

*****∀E drive county,home,airport,walk(car,S0);

10 (drivable(county,walk(car,S0))∧(at(home,county,walk(car,S0))∧(at(airport,county,walk(car,S0))∧(at(car,home,wa%
lk(car,S0))∧at(I,car,walk(car,S0))))))⊃(at(car,airport,drive(airport,walk(car,S0)))∧(∀x.(walkable(x,drive(airpor%
t,walk(car,S0)))≡walkable(x,walk(car,S0)))∧(∀x.(drivable(x,drive(airport,walk(car,S0)))≡drivable(x,walk(car,S0))%
)∧∀x y.((¬(x=car∨at(x,car,walk(car,S0)))∨y=car)⊃(at(x,y,drive(airport,walk(car,S0)))≡at(x,y,walk(car,S0)))))))  

*****TAUTEQ at(car,airport,drive(airport,walk(car,S0))) at3,at4,at5,notI,drivable,2,6:10;

11 at(car,airport,drive(airport,walk(car,S0)))  

*****∀E attrans I,car,airport,drive(airport,walk(car,S0));

12 (at(I,car,drive(airport,walk(car,S0)))∧at(car,airport,drive(airport,walk(car,S0))))⊃at(I,airport,drive(airpor%
t,walk(car,S0)))  

*****TAUTEQ ∀x y.((¬(x=car∨at(x,car,walk(car,S0)))∨y=car)⊃(at(x,y,drive(airport,walk(car,S0)))≡at(x,y,walk(car,S%
0)))) at3,at4,at5,notI,drivable,2,6:10;

13 ∀x y.((¬(x=car∨at(x,car,walk(car,S0)))∨y=car)⊃(at(x,y,drive(airport,walk(car,S0)))≡at(x,y,walk(car,S0))))  

*****∀E ↑ I,car;

14 (¬(I=car∨at(I,car,walk(car,S0)))∨car=car)⊃(at(I,car,drive(airport,walk(car,S0)))≡at(I,car,walk(car,S0)))  

*****TAUTEQ at(I,airport,drive(airport,walk(car,S0))) notI,2,11:12,14;

15 at(I,airport,drive(airport,walk(car,S0)))